ds:x:Id fp Type, da:k:Knd fp Type, k:Knd, l:IdLnk. msg-item(ds;da;k;l)  Type 

latex

Definitions	Id, t  T, Type, x. t(x), x:A. B(x), a:A fp B(a), Knd, IdLnk, Void, rcv(l,tg), KindDeq, x.A(x), f(x)?z, type List, Valtype(da;k), x:AB(x), State(ds), , x:AB(x), msg-item(ds;da;k;l)
Lemmas	nat wf, decl-state wf, ma-valtype wf, fpf-cap wf, Kind-deq wf, rcv wf, IdLnk wf, Knd wf, fpf wf, Id wf